a:, n:. (a  n)   

latex

Up	int 2, int 2
Definitions	False, P  Q, A, a  b  T , a  n, t  T, x:A. B(x), , S  T
Lemmas	nat plus wf, nat plus inc int nzero, eq int wf, divide wfa, le int wf, ifthenelse wf